package logicaDePredicados;

import java.util.Iterator;

import java.util.ListIterator;
import java.util.Stack;
import exceptions.UnBalancedExpressionException;
import exceptions.UnDecidibleValueException;
@Deprecated
public class LogicParser {

	private Sentence parsedSentence = null;
	private  Sentence postFixSentence = null;
	/**
	 * Parses and checks balance and decidability of the given sentence 
	 * @param sentence
	 * @return
	 * @throws UnBalancedExpressionException
	 * @throws UnDecidibleValueException
	 */
	public  boolean parseSentence(Sentence sentence)throws UnBalancedExpressionException,UnDecidibleValueException{
		parsedSentence = sentence;
		if (checkBalance(sentence)){
			/**
			 * put the sentence in Prenex Normal Form
			 */
			toPrenexNormalForm();
			postFixSentence=toPostFix(parsedSentence);			
			
			/*
			 * Check if the sentence has qualifiers or not, to decide how to evaluate it
			 */
			if (getLastQuantifierIndex()!=0)
			{
				return evaluateWithQuantifiers(postFixSentence);
			}else{
				return uDoTheMath(postFixSentence);
			}
		}else {
			throw new UnBalancedExpressionException ("unbalanced sentence");
		}

		//return uDoTheMath(postFixSentence);
	}
	private boolean uDoTheMath (Sentence aPostFixSentence) throws UnBalancedExpressionException, UnDecidibleValueException{
		Stack<Boolean> myStack = new Stack<Boolean>();
		Iterator <PredicateLogic> iterator = aPostFixSentence.getSentence().listIterator();
		PredicateLogic currentToken;
		while (iterator.hasNext()){
			currentToken=iterator.next();
			//if the token is an operand get its value and push it back to the stack
			if (isPredicate(currentToken)){
				PredicateLogic nextToken = iterator.next();
				if (nextToken.getClass().equals(PredicateConstant.class)){

					myStack.add(new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((PredicateConstant<?>)nextToken).getValue())));
				}
				if (nextToken.getClass().equals(PredicateVariable.class)){
					myStack.add(new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((PredicateVariable<?>)nextToken).getValue())));

				}
				/**
				 * if the parameter for the logic predicate is actually a Skolem Function, get the value of the function and therefore the value of the Logic predicate
				 */
				if (nextToken.getClass().equals(SkolemFunction.class)){
					/**
					 * get the next element, that should be either a constant or variable
					 */
					PredicateLogic skolemParameter = iterator.next();
					/**
					 * if it is a Variable, then treat it as one
					 */
					if (skolemParameter.getClass().equals(PredicateVariable.class)){
						myStack.add (new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((SkolemFunction<?, ?>)nextToken).calculate(((PredicateVariable<?>)skolemParameter).getValue()))));
					}else {
						/**
						 * if it is a constant, then treat it as one
						 */
						if (skolemParameter.getClass().equals(PredicateConstant.class)){

							myStack.add (new Boolean(((LogicPredicate<?>)currentToken).getTruthValue(((SkolemFunction<?, ?>)nextToken).calculate(((PredicateConstant<?>)skolemParameter).getValue()))));
						}
						else{
							/**
							 * otherwise, somehow the sentence is screwed up, so throw an exception
							 */
							throw new UnBalancedExpressionException ("PredicateVariable or PredicateConstant needed after SkolemFunction");
						}
					}
				}
			}
			// if it is an operator pop the operands needed and push back the result, 
			if (currentToken.getClass().equals(LogicOperator.class)){
				if (currentToken.equals(LogicOperatorFactory.createNOT())){
					if (myStack.isEmpty()){
						throw new UnBalancedExpressionException ("wrong expression");

					}
					else{
						Boolean temp= myStack.pop();
						myStack.push(new Boolean(!temp.booleanValue()));
					}

				}
				else
				{
					if (myStack.size()<2){
						throw new UnBalancedExpressionException ("missing operands");
					}else {
						if (currentToken.equals(LogicOperatorFactory.createAND())){
							Boolean q = myStack.pop();
							Boolean p= myStack.pop();
							myStack.push(new Boolean(p.booleanValue()&&q.booleanValue()));
						}
						if (currentToken.equals(LogicOperatorFactory.createOR())){
							Boolean q = myStack.pop();
							Boolean p= myStack.pop();
							myStack.push(new Boolean(p.booleanValue()||q.booleanValue()));
						}


					}

				}
			}
		}
		return myStack.pop().booleanValue();

	}
	/**
	 * returns true if the brackets are balanced or UnBalancedExpressionException if not.
	 * @param sentence
	 * @return
	 * @throws UnBalancedExpressionException
	 */
	private boolean checkBalance (Sentence sentence) throws UnBalancedExpressionException{
		int bracket=0;
		for (PredicateLogic i : sentence.getSentence()) {
			if (i.getName().equals(LogicOperatorFactory.createLeftBracket().getName())){
				bracket++;
			}
			if (i.getName().equals(LogicOperatorFactory.createRightBraket().getName())){
				bracket--;
			}
		}
		if (bracket!=0)
			throw new UnBalancedExpressionException ("Unbalanced Expression");
		return true;
	}

	/**
	 * converts the parsedSentence into prenex normal form
	 * @throws UnBalancedExpressionException 
	 */
	private void toPrenexNormalForm () throws UnBalancedExpressionException{

		int thenIndex = parsedSentence.indexOf(LogicOperatorFactory.createTHEN());
		if (thenIndex ==-1){
			return;
		}else {

			replaceThenWithConjunction(getLastQuantifierIndex(), parsedSentence.size()-1, thenIndex);
			replaceExistencialQuantifiers();
		}
		

	}
	/**
	 * replaces  "exists" with essential component and moves it to the beginning of the sentence if any
	 * @throws UnBalancedExpressionException 
	 */

	private void replaceExistencialQuantifiers () throws UnBalancedExpressionException{
		int existencialIndex=-1;
		PredicateLogic variable=null;
		if ((existencialIndex=parsedSentence.indexOf(LogicOperatorFactory.createExistentialQuantifier()))!=-1){
			parsedSentence.remove(existencialIndex);
			variable=parsedSentence.get(existencialIndex);
			parsedSentence.remove(existencialIndex);
			parsedSentence.add(existencialIndex,LogicOperatorFactory.createNOT());
			int toInsertIndex =getLastQuantifierIndex();
			parsedSentence.add(toInsertIndex, LogicOperatorFactory.createEssentialQuantifier());
			if (variable.getClass()!=PredicateVariable.class){
				throw new UnBalancedExpressionException("Quantifiers must be followed by Variables");
			}
			parsedSentence.add(toInsertIndex+1,variable);

			replaceExistencialQuantifiers();
		}
	}
	/**
	 * returns the index where the next Essential quantifier should be placed
	 * Example:
	 * ForAll x ForAll y (DOG ( X ) ) -> ( MAMMAL(Y)  )
	 * 
	 *     
	 * returns 3
	 * @return
	 */
	private int getLastQuantifierIndex (){
		ListIterator<PredicateLogic> iterator = parsedSentence.getSentence().listIterator();
		PredicateLogic term= iterator.next();
		while (iterator.hasNext()&&term.equals(LogicOperatorFactory.createEssentialQuantifier())){
			if (term.equals(LogicOperatorFactory.createEssentialQuantifier())){
				term=iterator.next();

			}

			term=iterator.next();
		}
		if (iterator.hasNext()){
			
			return iterator.previousIndex();
		}
		return 0;
	}
	/**
	 * replaces -> at thenIndex with OR and negate first term, inside the specified scope 
	 * P -> Q == ¬P v Q
	 * 
	 * @param scopeBegin
	 * @param scopeEnd
	 * @param thenIndex
	 */
	private void replaceThenWithConjunction (int scopeBegin, int scopeEnd, int thenIndex){
		parsedSentence.add(thenIndex,LogicOperatorFactory.createRightBraket());
		thenIndex++;
		scopeEnd++;
		parsedSentence.getSentence().add(thenIndex+1,LogicOperatorFactory.createLeftBracket());
		scopeEnd++;
		
		parsedSentence.getSentence().remove(thenIndex);
		scopeEnd--;
		parsedSentence.getSentence().add(thenIndex,LogicOperatorFactory.createOR());
		scopeEnd++;
		parsedSentence.getSentence().add(scopeBegin,LogicOperatorFactory.createLeftBracket());
		scopeEnd++;
		parsedSentence.getSentence().add(scopeBegin,LogicOperatorFactory.createNOT());
		scopeEnd++;
		parsedSentence.getSentence().add(scopeEnd+1,LogicOperatorFactory.createRightBraket());
		scopeEnd++;
		parsedSentence.toString();
	}
	/**
	 * Converts the proposition to prefix without including any Quantifiers. Needs Prenex Form proposition to work
	 * @param inFixSentence
	 * @return
	 * @throws UnBalancedExpressionException
	 */
	private Sentence toPostFix(Sentence inFixSentence)throws UnBalancedExpressionException {
		Stack<PredicateLogic> myStack = new Stack<PredicateLogic>();
		Sentence postFix=new Sentence ();
		
		Iterator <PredicateLogic>iterator = inFixSentence.getSentence().listIterator(getLastQuantifierIndex());
		while (iterator.hasNext()){
			try {

				PredicateLogic currentToken =  iterator.next();
				//If the token is an operand we simply add it to our answer.

				if (isOperand(currentToken)){

					postFix.add(currentToken);
					if (currentToken.getClass().equals(LogicPredicate.class)){
						postFix.add(iterator.next());
					
					}	

				}else {

					//If the token is an operator, and there's nothing else on our stack, we push that operator onto the stack. 
					if (currentToken.getClass().equals(LogicOperator.class) &&
							(!currentToken.equals(LogicOperatorFactory.createLeftBracket())||!currentToken.equals(LogicOperatorFactory.createLeftBracket()))&& myStack.isEmpty()){
						myStack.push(currentToken);

					}else {
						//If the token is a left parenthesis we simply push it onto the stack.
						if (currentToken.equals(LogicOperatorFactory.createLeftBracket()))
						{
							myStack.push(currentToken);

						}else{//operator is not a left parenthesis
							/**
							 * if the operator is a right parenthesis, we pop all the operators until the first left
							 * parenthesis. 
							 */
							if (currentToken.equals(LogicOperatorFactory.createRightBraket())){
								while (!myStack.peek().equals(LogicOperatorFactory.createLeftBracket())){

									postFix.add(myStack.pop());
									
								}
								myStack.pop();//pop the corresponding "(" 
							}else {
								/**
								 * If there is something on the stack, we compare the precedence of our current 
								 * operator with the one on the stack 
								 */
								if (!myStack.isEmpty()&&myStack.peek().equals(LogicOperatorFactory.createNOT())||currentToken.equals(LogicOperatorFactory.createNOT())){
									/**
									 * Handle unary operator before the rest of them
									 */

									if (currentToken.equals(LogicOperatorFactory.createNOT())){
										myStack.push(currentToken);

										
									}else {
										
									if (myStack.peek().equals(LogicOperatorFactory.createNOT())){
										postFix.add(myStack.pop());
										
										myStack.push(currentToken);
										
									}else
									{
										myStack.push(currentToken);


									}
									}

								}
							}
						}
					}
				}
			} catch (Exception e) {
				e.printStackTrace();
			}
		}
		while(! myStack.isEmpty()){
			postFix.add(myStack.pop());

		}

		return postFix;

	}
	/**
	 * Determines if the element is an operand or not. An operand would be a unary or 2-ary predicate
	 * @param element
	 * @return
	 */
	private boolean isOperand (PredicateLogic element){
		return (!element.getClass().equals(LogicOperator.class)&&(!element.getClass().equals(LogicQuantifier.class)));
	}
	/**
	 * Returns true if the element is a Predicate, or false if otherwise
	 * @param element
	 * @return
	 */
	private boolean isPredicate (PredicateLogic element){
		return isOperand(element)&& element.getClass().equals(LogicPredicate.class);
	}
	/**
	 * Evaluates whether the element is an operator or not. NOTE: higher precedence operators should considered individually
	 * @param element
	 * @return 
	 */
	private boolean isOperator (PredicateLogic element){
		return (element.getClass().equals(LogicOperator.class)||element.getClass().equals(LogicQuantifier.class));
	}
	/**
	 * Evaluates a sentence that has quantifiers and the respective variables.
	 * @param postFixSentence2 
	 * @return
	 * @throws UnBalancedExpressionException
	 * @throws UnDecidibleValueException
	 */
	private boolean evaluateWithQuantifiers (Sentence postFixSentence2) throws UnBalancedExpressionException, UnDecidibleValueException{
		
		return false;
	}
}
